Skip to content

convert smt to expr#103

Merged
agle merged 9 commits intomainfrom
smt_of_expr
Apr 13, 2026
Merged

convert smt to expr#103
agle merged 9 commits intomainfrom
smt_of_expr

Conversation

@agle
Copy link
Copy Markdown
Owner

@agle agle commented Mar 25, 2026

  • supports predicates and bvexprs that can be generated by bincaml
  • will not support all bvops defined in smtlib, we could extend it but it will need some translation into the IR (e.g. we don't define greater-than operators, so convert to not-lessthan).
  • expands expr gen property test to generate predicates
  • removes associative binary operators from Ops.AllOps.binary so they are only present in Ops.AllOps.intrin -- make their representation canonical

Copy link
Copy Markdown
Collaborator

@b-paul b-paul left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good (except for the one really small thing I noted), but I'd expect at least one thing to break if main is merged into this from binops being removed and turned into intrinsics only (at least one of my prs used them).

If you're busy I'm happy to handle the conflicts and whatnot, up to you

Comment thread lib/analysis/defuse_bool.ml Outdated
| `BVADD -> List.fold_left (eval_binary `BVADD) Bot args
| `BVOR -> List.fold_left (eval_binary `BVOR) Bot args
| `BVXOR -> List.fold_left (eval_binary `BVXOR) Bot args
| `BVMUL -> List.fold_left (eval_binary `BVXOR) Bot args
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

eval_binary `BVMUL?

@agle agle merged commit 3a5fcfd into main Apr 13, 2026
9 checks passed
@agle agle deleted the smt_of_expr branch April 13, 2026 06:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants